Inference at * 2 
Iof proof for Lemma primrec add:



1. T : Type
2. n : 
3. 0 < n
4. m:, b:T, c:({0..((n - 1)+m)}TT).
4. primrec((n - 1)+m;b;c) = primrec(n - 1;primrec(m;b;c);i,t. c(i+m,t))
5. m : 
6. b : T
7. c : {0..(n+m)}TT
  primrec(n+m;b;c) = primrec(n;primrec(m;b;c);i,t. c(i+m,t)) 

latex

 by ((InstHyp [m;b;c] 4) 
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 2:n),(first_nat 3:n
C)) (first_tok :t) inil_term))) 

latex

C1: 

C1: 8. primrec((n - 1)+m;b;c) = primrec(n - 1;primrec(m;b;c);i,t. c(i+m,t))
C1:   primrec(n+m;b;c) = primrec(n;primrec(m;b;c);i,t. c(i+m,t))
C.

Definitions	P & Q, i  j < k, suptype(S; T), S  T, t  T, {i..j}, x:A. B(x), , False, P  Q, A, A  B,
Lemmas	int seg wf, le wf